Dafny – Verification-Aware Programming Language
Formal verification aims to ensure that software behaves as intended by providing machine-checked proofs of correctness. Over the years, a range of tools have emerged to make verification more accessible and scalable.
Dafny is a verification-aware programming language developed by Rustan Leino (originally Microsoft Research) and his team (now AWS) . It combines specification, implementation, and verification in a single environment, supporting features like pre- and postconditions, loop invariants, and termination checking. The language itself is mature and expressive, with support for generics, classes, inductive datatypes, and more. This seminar explores both the Dafny language and its verification workflow, as well as its use of SMT solvers like Z3. Students are expected to verify a small but non-trivial program using Dafny to gain hands-on experience.